Topology-dependent behavior of wireless communication makes the modeling and verification of MOBILE Ad HOC NETWORKs (MANETs) more complicated. Reliable Restricted Broadcast Process Theory (RRBPT) was introduced to specify and analyze MANETs in an algebraic approach. Constrained Action Computation Tree Logic (CACLT), interpreted over the semantics of RRBPT, allows to specify topology-dependent properties of MANETs. However, model checking of CACTL formulae is restricted to MANETs with a small number of nodes or finite datatypes. Having an algebraic specification, the problem of model checking of CACTL properties can be reduced to solving Boolean equations, as an intermediate formalism. This technique has been followed in the mCRL2 toolset to verify -calculus properties extended with data. Having a sound translation from RRBPT to mCRL2, we can use its toolset to verify data-dependent properties of MANET processes with infinite state, data-dependent behaviors. By treating the topology-dependent behavior of CACTL modals as data, we can also verify topology-dependent behavior of MANETs. To this aim, we provide a sound translation from CACTL formulae to first order modal -calculus expressions. Our translation takes advantage of the formal treatment of data and parametrized propositional variables in the mCRL2 process and property specifications respectively to address the topology-formulae part of CACTL expressing multi-hop constrains over the topology.

In this paper, a brief review of most conventional routing protocols for MOBILE Ad- HOC NETWORKs has been conducted, moreover Dynamic Source Routing (DSR) protocol has been discussed with more details. The focuses on both route discovery and route maintaining phases as the main part of DSR protocol have been done and simulated in this paper. Random movement pattern for mobility of nodes have been assumed with random walk model. Also, negative exponential random model for time duration of a call. In addition with letting poisson distribution of a call demand, are assumed as the main problem definitions. Two main performance indices namely, call blocking and forced termination probabilities as constraints have been introduced. The above two indices for different loads and moving velocities have been simulated. In order to show the effects of Ad- HOC routing protocol on service quality. Two type of direct and indirect path servicing have been studied. Results shows that a multi loop path introduces lower blocking and forced termination rates.

MOBILE Ad HOC NETWORK (MANET) is a special and attractive type of new wireless NETWORKs. It is an autonomous system that can dynamically be set up anywhere and anytime without using any pre-existing NETWORK infrastructure and its MOBILE hosts are free to move randomly. Host mobility in MANET causes failure of wireless links between nodes and breaks all the routes that use these links.Consequently, route reconstructions are needed, which is one of the most crucial issues for this type of wireless NETWORKs. There are two common solutions to this problem which increase the route reliability (lifetime) in MANETs; increasing the reliability of the links by using more reliable links and multipath route discovery. In this paper, both these schemes are used to develop a reliable unicast routing protocol for MANETs. As the first step, an efficient cross layer link reliability metric is proposed for reliable link selection.Reliable routing protocols for MANETs use many link reliability metrics for finding reliable links; four of the most commonly used are: Link Expiration Time, Probabilistic Link Reliable Time, Link Packet Error Rate and Link Received Signal Strength. The cross layer metric combines the aforementioned metrics by means of a weight function. The value of the weighting factors of this function are determined by the Response Surface Methodology. Next a reliable position based clustering routing protocol is designed. In this protocol the MOBILE nodes form disjoint sets of clusters, and for increasing the stability of these clusters, the aforementioned cross layer link reliability metric is used for cluster formation. A route is constructed and represented by a sequence of clusters and more reliable links are selected for data transfer inside and between the clusters. Because of the multiple links which usually exist between the clusters, multipath route scheme is used in this routing protocol in addition to the reliable link selection. Simulation results show that by using this protocol the lowest number of route reconstructions is achieved in comparison with the other related protocols.

Over recent years, green communication technology has been emerged as an important area of concern for communication research and industrial community. The reason of paying attention of this area is its effect on reducing environmental pollutions. According to recent research, a significant share of these pollutions is produced by the local area computer NETWORKs. A MOBILE ad-HOC NETWORK (MANET) is one of the widely used local area NETWORKs. The energy efficiency is important in MANETs not only from the green communication point of view, but also due to the NETWORK limitations in terms of battery lifetime. Of course, MANETs characterization such as distributed nature and lack of administration, nodes mobility, frequent topology changes and scare resources makes the greening trend a challenging task in such a context. In this paper, we propose and implement a green routing protocol for MANET which solves the idle energy consumption by allowing the necessary nodes and switching off the other un-utilized nodes. Simulation results show this can help to the 20 percentage of saving energy in the environment on average and also aware of the quality of service.